Inductive tm : Set :=
  | new  : tp  -> tm
with tp : Set :=
  | tp_struct : list tm  -> tp.

Scheme tm_ind_3 := Induction for tm Sort Prop
  with tp_ind_3  := Induction for tp Sort Prop.
Print tm_ind_3.

